/-
Copyright (c) 2025 Jireh Loreaux. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jireh Loreaux
-/
module

public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
public import Mathlib.Topology.ContinuousMap.ContinuousSqrt

/-! # Range of the continuous functional calculus

This file contains results about the range of the continuous functional calculus, and
consequences thereof.

## Main results

* `range_cfcHom` and `range_cfcₙHom`: for `RCLike` scalar rings, the range of the continuous
  functional calculus homomorphism is the elemental subalgebra generated by the given element.
* `range_cfc_nnreal` and `range_cfcₙ_nnreal`: over the scalar semiring `ℝ≥0`, the range of the
  continuous functional calculus consists of the nonnegative elements in the elemental `ℝ`-algebra
  generated by the given element.

-/

@[expose] public section

open Topology

open scoped CStarAlgebra

section Unital

section RCLike

variable (𝕜 : Type*) {A : Type*} {p : A → Prop} [RCLike 𝕜] [Ring A] [StarRing A] [Algebra 𝕜 A]
variable [TopologicalSpace A] [StarModule 𝕜 A] [ContinuousFunctionalCalculus 𝕜 A p]
variable [IsTopologicalRing A] [ContinuousStar A]

open StarAlgebra

open scoped ContinuousFunctionalCalculus in
theorem range_cfcHom {a : A} (ha : p a) :
    (cfcHom ha (R := 𝕜)).range = elemental 𝕜 a := by
  rw [StarAlgHom.range_eq_map_top, ← ContinuousMap.elemental_id_eq_top, StarAlgebra.elemental,
    ← StarSubalgebra.topologicalClosure_map _ _ (cfcHom_isClosedEmbedding ha (R := 𝕜)).isClosedMap
      (cfcHom_continuous ha), StarAlgHom.map_adjoin]
  congr
  simpa using cfcHom_id ha

lemma range_cfc {a : A} (ha : p a) : Set.range (cfc (R := 𝕜) · a) = elemental 𝕜 a := by
  rw [range_cfc_eq_range_cfcHom 𝕜 ha, range_cfcHom 𝕜 ha]

variable {𝕜}

theorem cfcHom_apply_mem_elemental {a : A} (ha : p a) (f : C(spectrum 𝕜 a, 𝕜)) :
    cfcHom ha f ∈ elemental 𝕜 a :=
  range_cfcHom 𝕜 ha ▸ ⟨f, rfl⟩

@[simp, grind ←]
theorem cfc_apply_mem_elemental (f : 𝕜 → 𝕜) (a : A) :
    cfc f a ∈ elemental 𝕜 a :=
  cfc_cases _ a f (zero_mem _) fun hf ha ↦
    cfcHom_apply_mem_elemental ha ⟨_, hf.restrict⟩

end RCLike

open scoped NNReal
variable {A : Type*} [Ring A] [StarRing A] [Algebra ℝ A] [TopologicalSpace A]
variable [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [IsTopologicalRing A] [T2Space A]
variable [PartialOrder A] [NonnegSpectrumClass ℝ A] [StarOrderedRing A]

lemma range_cfc_nnreal_eq_image_cfc_real (a : A) (ha : 0 ≤ a) :
    Set.range (cfc (R := ℝ≥0) · a) = (cfc · a) '' {f | ∀ x ∈ spectrum ℝ a, 0 ≤ f x} := by
  ext
  constructor
  · rintro ⟨f, rfl⟩
    simp only [cfc_nnreal_eq_real f a ha]
    exact ⟨_, fun _ _ ↦ by positivity, rfl⟩
  · rintro ⟨f, hf, rfl⟩
    simp only [cfc_real_eq_nnreal a hf]
    exact ⟨_, rfl⟩

variable [ContinuousStar A] [StarModule ℝ A]

lemma range_cfc_nnreal (a : A) (ha : 0 ≤ a) :
    Set.range (cfc (R := ℝ≥0) · a) = {x | x ∈ StarAlgebra.elemental ℝ a ∧ 0 ≤ x} := by
  rw [range_cfc_nnreal_eq_image_cfc_real a ha, Set.setOf_and, SetLike.setOf_mem_eq,
    ← range_cfc _ ha.isSelfAdjoint, Set.inter_comm, ← Set.image_preimage_eq_inter_range]
  refine Set.Subset.antisymm (Set.image_mono (fun _ ↦ cfc_nonneg)) ?_
  rintro _ ⟨f, hf, rfl⟩
  simp only [Set.preimage_setOf_eq, Set.mem_setOf_eq, Set.mem_image] at hf ⊢
  obtain (⟨h₁, h₂⟩ | h | h) := by
    simpa only [not_and_or] using em (ContinuousOn f (spectrum ℝ a) ∧ IsSelfAdjoint a)
  · refine ⟨f, ?_, rfl⟩
    rwa [cfc_nonneg_iff f a] at hf
  · exact ⟨0, by simp, by simp [cfc_apply_of_not_continuousOn a h]⟩
  · exact ⟨0, by simp, by simp [cfc_apply_of_not_predicate a h]⟩

end Unital

section NonUnital

section RCLike

variable (𝕜 : Type*) {A : Type*} {p : A → Prop} [RCLike 𝕜] [NonUnitalRing A] [StarRing A]
variable [Module 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A]
variable [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus 𝕜 A p]
variable [ContinuousConstSMul 𝕜 A] [StarModule 𝕜 A] [IsTopologicalRing A] [ContinuousStar A]

open NonUnitalStarAlgebra

open scoped NonUnitalContinuousFunctionalCalculus in
theorem range_cfcₙHom {a : A} (ha : p a) :
    NonUnitalStarAlgHom.range (cfcₙHom ha (R := 𝕜)) = elemental 𝕜 a := by
  rw [← NonUnitalStarAlgebra.map_top, ← ContinuousMapZero.elemental_eq_top,
    NonUnitalStarAlgebra.elemental, ← NonUnitalStarSubalgebra.topologicalClosure_map _
    (cfcₙHom_isClosedEmbedding ha (R := 𝕜)).isClosedMap (cfcₙHom_continuous ha),
    NonUnitalStarAlgHom.map_adjoin]
  congr
  simpa using cfcₙHom_id ha

theorem range_cfcₙ {a : A} (ha : p a) : Set.range (cfcₙ (R := 𝕜) · a) = elemental 𝕜 a := by
  rw [range_cfcₙ_eq_range_cfcₙHom 𝕜 ha, range_cfcₙHom 𝕜 ha]

variable {𝕜}

open scoped ContinuousMapZero

theorem cfcₙHom_apply_mem_elemental {a : A} (ha : p a) (f : C(quasispectrum 𝕜 a, 𝕜)₀) :
    cfcₙHom ha f ∈ elemental 𝕜 a :=
  range_cfcₙHom 𝕜 ha ▸ ⟨f, rfl⟩

@[simp, grind ←]
theorem cfcₙ_apply_mem_elemental (f : 𝕜 → 𝕜) (a : A) :
    cfcₙ f a ∈ elemental 𝕜 a :=
  cfcₙ_cases _ a f (zero_mem _) fun hf hf₀ ha ↦
    cfcₙHom_apply_mem_elemental ha ⟨⟨_, hf.restrict⟩, hf₀⟩

end RCLike

open scoped NNReal
variable {A : Type*} [NonUnitalRing A] [StarRing A] [Module ℝ A] [IsScalarTower ℝ A A]
variable [SMulCommClass ℝ A A] [TopologicalSpace A]
variable [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [IsTopologicalRing A] [T2Space A]
variable [PartialOrder A] [NonnegSpectrumClass ℝ A] [StarOrderedRing A]

lemma range_cfcₙ_nnreal_eq_image_cfcₙ_real (a : A) (ha : 0 ≤ a) :
    Set.range (cfcₙ (R := ℝ≥0) · a) = (cfcₙ · a) '' {f | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x} := by
  ext
  constructor
  · rintro ⟨f, rfl⟩
    simp only [cfcₙ_nnreal_eq_real f a]
    exact ⟨_, fun _ _ ↦ by positivity, rfl⟩
  · rintro ⟨f, hf, rfl⟩
    simp only [cfcₙ_real_eq_nnreal a hf]
    exact ⟨_, rfl⟩

variable [StarModule ℝ A] [ContinuousStar A] [ContinuousConstSMul ℝ A]

lemma range_cfcₙ_nnreal (a : A) (ha : 0 ≤ a) :
    Set.range (cfcₙ (R := ℝ≥0) · a) = {x | x ∈ NonUnitalStarAlgebra.elemental ℝ a ∧ 0 ≤ x} := by
  rw [range_cfcₙ_nnreal_eq_image_cfcₙ_real a ha, Set.setOf_and, SetLike.setOf_mem_eq,
    ← range_cfcₙ _ ha.isSelfAdjoint, Set.inter_comm, ← Set.image_preimage_eq_inter_range]
  refine Set.Subset.antisymm (Set.image_mono (fun _ ↦ cfcₙ_nonneg)) ?_
  rintro _ ⟨f, hf, rfl⟩
  simp only [Set.preimage_setOf_eq, Set.mem_setOf_eq, Set.mem_image] at hf ⊢
  obtain (⟨h₁, h₂, h₃⟩ | h | h | h) := by
    simpa only [not_and_or] using
      em (ContinuousOn f (quasispectrum ℝ a) ∧ f 0 = 0 ∧ IsSelfAdjoint a)
  · refine ⟨f, ?_, rfl⟩
    rwa [cfcₙ_nonneg_iff f a] at hf
  · exact ⟨0, by simp, by simp [cfcₙ_apply_of_not_continuousOn a h]⟩
  · exact ⟨0, by simp, by simp [cfcₙ_apply_of_not_map_zero a h]⟩
  · exact ⟨0, by simp, by simp [cfcₙ_apply_of_not_predicate a h]⟩

end NonUnital
